(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")


(declare-fun |main::a@3| () Real)
(declare-fun |__ADDRESS_OF_main::a| () Real)
(declare-fun *signed_int@1 (Real) Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun *signed_int@2 (Real) Real)
(declare-fun |main::q@3| () Real)
(declare-fun |__ADDRESS_OF_main::q| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real |__ADDRESS_OF_main::a|)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Bool (<= _8 _7))
(define-fun _12 () Bool (not _11))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real |__ADDRESS_OF_main::q|)
(define-fun _15 () Real (__BASE_ADDRESS_OF__ _14))
(define-fun _16 () Bool (= _14 _15))
(define-fun _17 () Bool (and _13 _16))
(define-fun _18 () Real 1)
(define-fun _19 () Real |main::a@3|)
(define-fun _20 () Bool (= _19 _18))
(define-fun _21 () Bool (and _17 _20))
(define-fun _22 () Real (*signed_int@1 _8))
(define-fun _23 () Bool (= _19 _22))
(define-fun _24 () Real |main::q@3|)
(define-fun _25 () Bool (= _8 _24))
(define-fun _26 () Bool (and _23 _25))
(define-fun _27 () Bool (and _21 _26))
(define-fun _28 () Real 2)
(define-fun _29 () Real (*signed_int@2 _24))
(define-fun _30 () Bool (= _29 _28))
(define-fun _31 () Real (*signed_int@2 _8))
(define-fun _32 () Bool (= _22 _31))
(define-fun _33 () Bool (or _25 _32))
(define-fun _34 () Bool (and _30 _33))
(define-fun _35 () Bool (and _27 _34))
(define-fun _36 () Bool (= _31 _28))
(define-fun _37 () Bool (not _36))
(define-fun _39 () Bool (and _35 _37))
(define-fun _2 () Bool false)


(push 1)
(assert _39)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)
